Nuprl Lemma : rel_plus_functionality_wrt_breqv
11,40
postcript
pdf
T
:Type,
R1
,
R2
:(
T
T
). (
R1
<
>{
T
}
R2
)
(
R1
^+ <
>{
T
}
R2
^+)
latex
Definitions
x
:
A
B
(
x
)
,
,
Type
,
E
<
>{
T
}
E'
,
R
^+
,
x
:
A
.
B
(
x
)
,
P
Q
Lemmas
binrel
le
weakening
,
binrel
eqv
inversion
,
rel
plus
functionality
wrt
brle
,
binrel
le
antisymmetry
origin
T:Type, R1, R2:(T
T
). (R1 <
>{T} R2) 
(R1^+ <>{T} R2^+) T:Type, R1, R2:(TT). (R1 <>{T} R2) (R1^+ <>{T} R2^+) B(x)>{T} E'x:A. B(x) Q